'Weak Dependency Graph [60.0]'
------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, proper(f(X)) -> f(proper(X))
, proper(0()) -> ok(0())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(ok(X)) -> ok(f(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, top(mark(X)) -> top(proper(X))
, top(ok(X)) -> top(active(X))}
Details:
We have computed the following set of weak (innermost) dependency pairs:
{ active^#(f(0())) -> c_0(cons^#(0(), f(s(0()))))
, active^#(f(s(0()))) -> c_1(f^#(p(s(0()))))
, active^#(p(s(X))) -> c_2()
, active^#(f(X)) -> c_3(f^#(active(X)))
, active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))
, active^#(s(X)) -> c_5(s^#(active(X)))
, active^#(p(X)) -> c_6(p^#(active(X)))
, f^#(mark(X)) -> c_7(f^#(X))
, cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))
, s^#(mark(X)) -> c_9(s^#(X))
, p^#(mark(X)) -> c_10(p^#(X))
, proper^#(f(X)) -> c_11(f^#(proper(X)))
, proper^#(0()) -> c_12()
, proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2)))
, proper^#(s(X)) -> c_14(s^#(proper(X)))
, proper^#(p(X)) -> c_15(p^#(proper(X)))
, f^#(ok(X)) -> c_16(f^#(X))
, cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))
, s^#(ok(X)) -> c_18(s^#(X))
, p^#(ok(X)) -> c_19(p^#(X))
, top^#(mark(X)) -> c_20(top^#(proper(X)))
, top^#(ok(X)) -> c_21(top^#(active(X)))}
The usable rules are:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, proper(f(X)) -> f(proper(X))
, proper(0()) -> ok(0())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
The estimated dependency graph contains the following edges:
{active^#(f(X)) -> c_3(f^#(active(X)))}
==> {f^#(ok(X)) -> c_16(f^#(X))}
{active^#(f(X)) -> c_3(f^#(active(X)))}
==> {f^#(mark(X)) -> c_7(f^#(X))}
{active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))}
==> {cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))}
{active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))}
==> {cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))}
{active^#(s(X)) -> c_5(s^#(active(X)))}
==> {s^#(ok(X)) -> c_18(s^#(X))}
{active^#(s(X)) -> c_5(s^#(active(X)))}
==> {s^#(mark(X)) -> c_9(s^#(X))}
{active^#(p(X)) -> c_6(p^#(active(X)))}
==> {p^#(ok(X)) -> c_19(p^#(X))}
{active^#(p(X)) -> c_6(p^#(active(X)))}
==> {p^#(mark(X)) -> c_10(p^#(X))}
{f^#(mark(X)) -> c_7(f^#(X))}
==> {f^#(ok(X)) -> c_16(f^#(X))}
{f^#(mark(X)) -> c_7(f^#(X))}
==> {f^#(mark(X)) -> c_7(f^#(X))}
{cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))}
==> {cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))}
{cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))}
==> {cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))}
{s^#(mark(X)) -> c_9(s^#(X))}
==> {s^#(ok(X)) -> c_18(s^#(X))}
{s^#(mark(X)) -> c_9(s^#(X))}
==> {s^#(mark(X)) -> c_9(s^#(X))}
{p^#(mark(X)) -> c_10(p^#(X))}
==> {p^#(ok(X)) -> c_19(p^#(X))}
{p^#(mark(X)) -> c_10(p^#(X))}
==> {p^#(mark(X)) -> c_10(p^#(X))}
{proper^#(f(X)) -> c_11(f^#(proper(X)))}
==> {f^#(ok(X)) -> c_16(f^#(X))}
{proper^#(f(X)) -> c_11(f^#(proper(X)))}
==> {f^#(mark(X)) -> c_7(f^#(X))}
{proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2)))}
==> {cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))}
{proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2)))}
==> {cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))}
{proper^#(s(X)) -> c_14(s^#(proper(X)))}
==> {s^#(ok(X)) -> c_18(s^#(X))}
{proper^#(s(X)) -> c_14(s^#(proper(X)))}
==> {s^#(mark(X)) -> c_9(s^#(X))}
{proper^#(p(X)) -> c_15(p^#(proper(X)))}
==> {p^#(ok(X)) -> c_19(p^#(X))}
{proper^#(p(X)) -> c_15(p^#(proper(X)))}
==> {p^#(mark(X)) -> c_10(p^#(X))}
{f^#(ok(X)) -> c_16(f^#(X))}
==> {f^#(ok(X)) -> c_16(f^#(X))}
{f^#(ok(X)) -> c_16(f^#(X))}
==> {f^#(mark(X)) -> c_7(f^#(X))}
{cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))}
==> {cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))}
{cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))}
==> {cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))}
{s^#(ok(X)) -> c_18(s^#(X))}
==> {s^#(ok(X)) -> c_18(s^#(X))}
{s^#(ok(X)) -> c_18(s^#(X))}
==> {s^#(mark(X)) -> c_9(s^#(X))}
{p^#(ok(X)) -> c_19(p^#(X))}
==> {p^#(ok(X)) -> c_19(p^#(X))}
{p^#(ok(X)) -> c_19(p^#(X))}
==> {p^#(mark(X)) -> c_10(p^#(X))}
{top^#(mark(X)) -> c_20(top^#(proper(X)))}
==> {top^#(ok(X)) -> c_21(top^#(active(X)))}
{top^#(mark(X)) -> c_20(top^#(proper(X)))}
==> {top^#(mark(X)) -> c_20(top^#(proper(X)))}
{top^#(ok(X)) -> c_21(top^#(active(X)))}
==> {top^#(ok(X)) -> c_21(top^#(active(X)))}
{top^#(ok(X)) -> c_21(top^#(active(X)))}
==> {top^#(mark(X)) -> c_20(top^#(proper(X)))}
We consider the following path(s):
1) { top^#(mark(X)) -> c_20(top^#(proper(X)))
, top^#(ok(X)) -> c_21(top^#(active(X)))}
The usable rules for this path are the following:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, proper(f(X)) -> f(proper(X))
, proper(0()) -> ok(0())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, proper(f(X)) -> f(proper(X))
, proper(0()) -> ok(0())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, top^#(mark(X)) -> c_20(top^#(proper(X)))
, top^#(ok(X)) -> c_21(top^#(active(X)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ proper(0()) -> ok(0())
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ proper(0()) -> ok(0())
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [9]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [1] x1 + [8]
c_20(x1) = [1] x1 + [0]
c_21(x1) = [1] x1 + [8]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{top^#(ok(X)) -> c_21(top^#(active(X)))}
and weakly orienting the rules
{ proper(0()) -> ok(0())
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{top^#(ok(X)) -> c_21(top^#(active(X)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [9]
ok(x1) = [1] x1 + [8]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [1] x1 + [1]
c_20(x1) = [1] x1 + [0]
c_21(x1) = [1] x1 + [1]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)}
and weakly orienting the rules
{ top^#(ok(X)) -> c_21(top^#(active(X)))
, proper(0()) -> ok(0())
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [2]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [7]
ok(x1) = [1] x1 + [4]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [1] x1 + [0]
c_20(x1) = [1] x1 + [9]
c_21(x1) = [1] x1 + [3]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active(f(0())) -> mark(cons(0(), f(s(0()))))}
and weakly orienting the rules
{ active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, top^#(ok(X)) -> c_21(top^#(active(X)))
, proper(0()) -> ok(0())
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(f(0())) -> mark(cons(0(), f(s(0()))))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [8]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [6]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [10]
ok(x1) = [1] x1 + [8]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [1] x1 + [4]
c_20(x1) = [1] x1 + [1]
c_21(x1) = [1] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, proper(f(X)) -> f(proper(X))
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, top^#(mark(X)) -> c_20(top^#(proper(X)))}
Weak Rules:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, top^#(ok(X)) -> c_21(top^#(active(X)))
, proper(0()) -> ok(0())
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, proper(f(X)) -> f(proper(X))
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, top^#(mark(X)) -> c_20(top^#(proper(X)))}
Weak Rules:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, top^#(ok(X)) -> c_21(top^#(active(X)))
, proper(0()) -> ok(0())
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
The problem is Match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ active_0(2) -> 4
, active_1(2) -> 8
, active_1(9) -> 11
, 0_0() -> 2
, 0_1() -> 9
, mark_0(2) -> 2
, proper_1(2) -> 6
, ok_0(2) -> 2
, ok_1(9) -> 6
, top^#_0(2) -> 1
, top^#_0(4) -> 3
, top^#_1(6) -> 5
, top^#_1(8) -> 7
, top^#_1(11) -> 10
, c_20_1(5) -> 1
, c_21_0(3) -> 1
, c_21_1(7) -> 1
, c_21_1(10) -> 5}
2) { active^#(p(X)) -> c_6(p^#(active(X)))
, p^#(ok(X)) -> c_19(p^#(X))
, p^#(mark(X)) -> c_10(p^#(X))}
The usable rules for this path are the following:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, active^#(p(X)) -> c_6(p^#(active(X)))
, p^#(ok(X)) -> c_19(p^#(X))
, p^#(mark(X)) -> c_10(p^#(X))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ active(p(s(X))) -> mark(X)
, active^#(p(X)) -> c_6(p^#(active(X)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ active(p(s(X))) -> mark(X)
, active^#(p(X)) -> c_6(p^#(active(X)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [7]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [9]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [1] x1 + [1]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{p^#(mark(X)) -> c_10(p^#(X))}
and weakly orienting the rules
{ active(p(s(X))) -> mark(X)
, active^#(p(X)) -> c_6(p^#(active(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{p^#(mark(X)) -> c_10(p^#(X))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [1]
p^#(x1) = [1] x1 + [7]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [1] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
and weakly orienting the rules
{ p^#(mark(X)) -> c_10(p^#(X))
, active(p(s(X))) -> mark(X)
, active^#(p(X)) -> c_6(p^#(active(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [2]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [1]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [1] x1 + [1]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{p^#(ok(X)) -> c_19(p^#(X))}
and weakly orienting the rules
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, p^#(mark(X)) -> c_10(p^#(X))
, active(p(s(X))) -> mark(X)
, active^#(p(X)) -> c_6(p^#(active(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{p^#(ok(X)) -> c_19(p^#(X))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [2]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [15]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [1]
p^#(x1) = [1] x1 + [15]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [1] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active(f(s(0()))) -> mark(f(p(s(0()))))}
and weakly orienting the rules
{ p^#(ok(X)) -> c_19(p^#(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, p^#(mark(X)) -> c_10(p^#(X))
, active(p(s(X))) -> mark(X)
, active^#(p(X)) -> c_6(p^#(active(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(f(s(0()))) -> mark(f(p(s(0()))))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [6]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [8]
s(x1) = [1] x1 + [1]
p(x1) = [1] x1 + [1]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [15]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
p^#(x1) = [1] x1 + [4]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [1] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active(f(0())) -> mark(cons(0(), f(s(0()))))}
and weakly orienting the rules
{ active(f(s(0()))) -> mark(f(p(s(0()))))
, p^#(ok(X)) -> c_19(p^#(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, p^#(mark(X)) -> c_10(p^#(X))
, active(p(s(X))) -> mark(X)
, active^#(p(X)) -> c_6(p^#(active(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(f(0())) -> mark(cons(0(), f(s(0()))))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [3]
p^#(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [1] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, p^#(ok(X)) -> c_19(p^#(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, p^#(mark(X)) -> c_10(p^#(X))
, active(p(s(X))) -> mark(X)
, active^#(p(X)) -> c_6(p^#(active(X)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, p^#(ok(X)) -> c_19(p^#(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, p^#(mark(X)) -> c_10(p^#(X))
, active(p(s(X))) -> mark(X)
, active^#(p(X)) -> c_6(p^#(active(X)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ 0_0() -> 3
, mark_0(3) -> 4
, mark_0(4) -> 4
, mark_0(9) -> 4
, ok_0(3) -> 9
, ok_0(4) -> 9
, ok_0(9) -> 9
, active^#_0(3) -> 11
, active^#_0(4) -> 11
, active^#_0(9) -> 11
, p^#_0(3) -> 22
, p^#_0(4) -> 22
, p^#_0(9) -> 22
, c_10_0(22) -> 22
, c_19_0(22) -> 22}
3) { active^#(s(X)) -> c_5(s^#(active(X)))
, s^#(ok(X)) -> c_18(s^#(X))
, s^#(mark(X)) -> c_9(s^#(X))}
The usable rules for this path are the following:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, active^#(s(X)) -> c_5(s^#(active(X)))
, s^#(ok(X)) -> c_18(s^#(X))
, s^#(mark(X)) -> c_9(s^#(X))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ active(p(s(X))) -> mark(X)
, s^#(mark(X)) -> c_9(s^#(X))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ active(p(s(X))) -> mark(X)
, s^#(mark(X)) -> c_9(s^#(X))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [8]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
s^#(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [1] x1 + [1]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active^#(s(X)) -> c_5(s^#(active(X)))}
and weakly orienting the rules
{ active(p(s(X))) -> mark(X)
, s^#(mark(X)) -> c_9(s^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(s(X)) -> c_5(s^#(active(X)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [13]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [1]
s^#(x1) = [1] x1 + [9]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [1] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
and weakly orienting the rules
{ active^#(s(X)) -> c_5(s^#(active(X)))
, active(p(s(X))) -> mark(X)
, s^#(mark(X)) -> c_9(s^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [2]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
s^#(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [1]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [1] x1 + [1]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{s^#(ok(X)) -> c_18(s^#(X))}
and weakly orienting the rules
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, active^#(s(X)) -> c_5(s^#(active(X)))
, active(p(s(X))) -> mark(X)
, s^#(mark(X)) -> c_9(s^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{s^#(ok(X)) -> c_18(s^#(X))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [2]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [3]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [11]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
s^#(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [1]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [1] x1 + [1]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))}
and weakly orienting the rules
{ s^#(ok(X)) -> c_18(s^#(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, active^#(s(X)) -> c_5(s^#(active(X)))
, active(p(s(X))) -> mark(X)
, s^#(mark(X)) -> c_9(s^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [7]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [1]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [15]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
s^#(x1) = [1] x1 + [8]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [1] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, s^#(ok(X)) -> c_18(s^#(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, active^#(s(X)) -> c_5(s^#(active(X)))
, active(p(s(X))) -> mark(X)
, s^#(mark(X)) -> c_9(s^#(X))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, s^#(ok(X)) -> c_18(s^#(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, active^#(s(X)) -> c_5(s^#(active(X)))
, active(p(s(X))) -> mark(X)
, s^#(mark(X)) -> c_9(s^#(X))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ 0_0() -> 2
, mark_0(2) -> 2
, ok_0(2) -> 2
, active^#_0(2) -> 1
, s^#_0(2) -> 1
, c_9_0(1) -> 1
, c_18_0(1) -> 1}
4) { active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))
, cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))
, cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))}
The usable rules for this path are the following:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))
, cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))
, cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))}
Details:
We apply the weight gap principle, strictly orienting the rules
{cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [7]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [1] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [1] x1 + [1]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))}
and weakly orienting the rules
{cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [2]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [5]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [1] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [1] x1 + [1]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))}
and weakly orienting the rules
{ active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))
, cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [4]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [1]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [1]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [1] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [1] x1 + [7]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active(p(s(X))) -> mark(X)}
and weakly orienting the rules
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))
, active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))
, cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(p(s(X))) -> mark(X)}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [8]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [1] x1 + [1]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [1] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))}
and weakly orienting the rules
{ active(p(s(X))) -> mark(X)
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))
, active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))
, cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [8]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [1]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [6]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [1] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [1] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))
, active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))
, cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))
, active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))
, cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ 0_0() -> 3
, mark_0(3) -> 4
, mark_0(4) -> 4
, mark_0(9) -> 4
, ok_0(3) -> 9
, ok_0(4) -> 9
, ok_0(9) -> 9
, active^#_0(3) -> 11
, active^#_0(4) -> 11
, active^#_0(9) -> 11
, cons^#_0(3, 3) -> 13
, cons^#_0(3, 4) -> 13
, cons^#_0(3, 9) -> 13
, cons^#_0(4, 3) -> 13
, cons^#_0(4, 4) -> 13
, cons^#_0(4, 9) -> 13
, cons^#_0(9, 3) -> 13
, cons^#_0(9, 4) -> 13
, cons^#_0(9, 9) -> 13
, c_8_0(13) -> 13
, c_17_0(13) -> 13}
5) { active^#(f(X)) -> c_3(f^#(active(X)))
, f^#(ok(X)) -> c_16(f^#(X))
, f^#(mark(X)) -> c_7(f^#(X))}
The usable rules for this path are the following:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, active^#(f(X)) -> c_3(f^#(active(X)))
, f^#(ok(X)) -> c_16(f^#(X))
, f^#(mark(X)) -> c_7(f^#(X))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ active(p(s(X))) -> mark(X)
, f^#(mark(X)) -> c_7(f^#(X))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ active(p(s(X))) -> mark(X)
, f^#(mark(X)) -> c_7(f^#(X))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [8]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_2() = [0]
c_3(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [1] x1 + [1]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, f^#(ok(X)) -> c_16(f^#(X))}
and weakly orienting the rules
{ active(p(s(X))) -> mark(X)
, f^#(mark(X)) -> c_7(f^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, f^#(ok(X)) -> c_16(f^#(X))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [8]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [2]
c_2() = [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [1]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [1] x1 + [1]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active^#(f(X)) -> c_3(f^#(active(X)))}
and weakly orienting the rules
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, f^#(ok(X)) -> c_16(f^#(X))
, active(p(s(X))) -> mark(X)
, f^#(mark(X)) -> c_7(f^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(f(X)) -> c_3(f^#(active(X)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [5]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [3]
c_2() = [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [1] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))}
and weakly orienting the rules
{ active^#(f(X)) -> c_3(f^#(active(X)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, f^#(ok(X)) -> c_16(f^#(X))
, active(p(s(X))) -> mark(X)
, f^#(mark(X)) -> c_7(f^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [2]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [1]
p(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [3]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [1]
c_2() = [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [1] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active^#(f(X)) -> c_3(f^#(active(X)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, f^#(ok(X)) -> c_16(f^#(X))
, active(p(s(X))) -> mark(X)
, f^#(mark(X)) -> c_7(f^#(X))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active^#(f(X)) -> c_3(f^#(active(X)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, f^#(ok(X)) -> c_16(f^#(X))
, active(p(s(X))) -> mark(X)
, f^#(mark(X)) -> c_7(f^#(X))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ 0_0() -> 3
, mark_0(3) -> 4
, mark_0(4) -> 4
, mark_0(9) -> 4
, ok_0(3) -> 9
, ok_0(4) -> 9
, ok_0(9) -> 9
, active^#_0(3) -> 11
, active^#_0(4) -> 11
, active^#_0(9) -> 11
, f^#_0(3) -> 15
, f^#_0(4) -> 15
, f^#_0(9) -> 15
, c_7_0(15) -> 15
, c_16_0(15) -> 15}
6) {active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))}
The usable rules for this path are the following:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ active(p(s(X))) -> mark(X)
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ active(p(s(X))) -> mark(X)
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [6]
p(x1) = [1] x1 + [1]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [2]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))}
and weakly orienting the rules
{ active(p(s(X))) -> mark(X)
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [5]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [2]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active(f(s(0()))) -> mark(f(p(s(0()))))}
and weakly orienting the rules
{ active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))
, active(p(s(X))) -> mark(X)
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(f(s(0()))) -> mark(f(p(s(0()))))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [3]
f(x1) = [1] x1 + [0]
0() = [2]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [3]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active(f(0())) -> mark(cons(0(), f(s(0()))))}
and weakly orienting the rules
{ active(f(s(0()))) -> mark(f(p(s(0()))))
, active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))
, active(p(s(X))) -> mark(X)
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(f(0())) -> mark(cons(0(), f(s(0()))))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [2]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [7]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [4]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))
, active(p(s(X))) -> mark(X)
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active^#(cons(X1, X2)) -> c_4(cons^#(active(X1), X2))
, active(p(s(X))) -> mark(X)
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ 0_0() -> 3
, mark_0(3) -> 4
, mark_0(4) -> 4
, mark_0(9) -> 4
, ok_0(3) -> 9
, ok_0(4) -> 9
, ok_0(9) -> 9
, active^#_0(3) -> 11
, active^#_0(4) -> 11
, active^#_0(9) -> 11
, cons^#_0(3, 3) -> 13
, cons^#_0(3, 4) -> 13
, cons^#_0(3, 9) -> 13
, cons^#_0(4, 3) -> 13
, cons^#_0(4, 4) -> 13
, cons^#_0(4, 9) -> 13
, cons^#_0(9, 3) -> 13
, cons^#_0(9, 4) -> 13
, cons^#_0(9, 9) -> 13}
7) { proper^#(s(X)) -> c_14(s^#(proper(X)))
, s^#(ok(X)) -> c_18(s^#(X))
, s^#(mark(X)) -> c_9(s^#(X))}
The usable rules for this path are the following:
{ proper(f(X)) -> f(proper(X))
, proper(0()) -> ok(0())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(f(X)) -> f(proper(X))
, proper(0()) -> ok(0())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, proper^#(s(X)) -> c_14(s^#(proper(X)))
, s^#(ok(X)) -> c_18(s^#(X))
, s^#(mark(X)) -> c_9(s^#(X))}
Details:
We apply the weight gap principle, strictly orienting the rules
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [1]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [1]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [1] x1 + [1]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{s^#(ok(X)) -> c_18(s^#(X))}
and weakly orienting the rules
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{s^#(ok(X)) -> c_18(s^#(X))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [1]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [1]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [2]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [1] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{s^#(mark(X)) -> c_9(s^#(X))}
and weakly orienting the rules
{ s^#(ok(X)) -> c_18(s^#(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{s^#(mark(X)) -> c_9(s^#(X))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [2]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [1]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [1]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [1] x1 + [1]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper^#(s(X)) -> c_14(s^#(proper(X)))}
and weakly orienting the rules
{ s^#(mark(X)) -> c_9(s^#(X))
, s^#(ok(X)) -> c_18(s^#(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(s(X)) -> c_14(s^#(proper(X)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [1] x1 + [1]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [1]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [1] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper(0()) -> ok(0())}
and weakly orienting the rules
{ proper^#(s(X)) -> c_14(s^#(proper(X)))
, s^#(mark(X)) -> c_9(s^#(X))
, s^#(ok(X)) -> c_18(s^#(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper(0()) -> ok(0())}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [5]
ok(x1) = [1] x1 + [4]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [5]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [1] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ proper(0()) -> ok(0())
, proper^#(s(X)) -> c_14(s^#(proper(X)))
, s^#(mark(X)) -> c_9(s^#(X))
, s^#(ok(X)) -> c_18(s^#(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ proper(0()) -> ok(0())
, proper^#(s(X)) -> c_14(s^#(proper(X)))
, s^#(mark(X)) -> c_9(s^#(X))
, s^#(ok(X)) -> c_18(s^#(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ 0_0() -> 3
, mark_0(3) -> 4
, mark_0(4) -> 4
, mark_0(9) -> 4
, ok_0(3) -> 9
, ok_0(4) -> 9
, ok_0(9) -> 9
, s^#_0(3) -> 20
, s^#_0(4) -> 20
, s^#_0(9) -> 20
, c_9_0(20) -> 20
, proper^#_0(3) -> 27
, proper^#_0(4) -> 27
, proper^#_0(9) -> 27
, c_18_0(20) -> 20}
8) { proper^#(p(X)) -> c_15(p^#(proper(X)))
, p^#(ok(X)) -> c_19(p^#(X))
, p^#(mark(X)) -> c_10(p^#(X))}
The usable rules for this path are the following:
{ proper(f(X)) -> f(proper(X))
, proper(0()) -> ok(0())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(f(X)) -> f(proper(X))
, proper(0()) -> ok(0())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, proper^#(p(X)) -> c_15(p^#(proper(X)))
, p^#(ok(X)) -> c_19(p^#(X))
, p^#(mark(X)) -> c_10(p^#(X))}
Details:
We apply the weight gap principle, strictly orienting the rules
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [1]
proper^#(x1) = [1] x1 + [1]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [1] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [1] x1 + [1]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{p^#(ok(X)) -> c_19(p^#(X))}
and weakly orienting the rules
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{p^#(ok(X)) -> c_19(p^#(X))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [1]
proper^#(x1) = [1] x1 + [1]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [1] x1 + [1]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [1] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{p^#(mark(X)) -> c_10(p^#(X))}
and weakly orienting the rules
{ p^#(ok(X)) -> c_19(p^#(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{p^#(mark(X)) -> c_10(p^#(X))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [2]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [1]
proper^#(x1) = [1] x1 + [1]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [1] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [1] x1 + [1]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper^#(p(X)) -> c_15(p^#(proper(X)))}
and weakly orienting the rules
{ p^#(mark(X)) -> c_10(p^#(X))
, p^#(ok(X)) -> c_19(p^#(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(p(X)) -> c_15(p^#(proper(X)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [1] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [1] x1 + [1]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper(0()) -> ok(0())}
and weakly orienting the rules
{ proper^#(p(X)) -> c_15(p^#(proper(X)))
, p^#(mark(X)) -> c_10(p^#(X))
, p^#(ok(X)) -> c_19(p^#(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper(0()) -> ok(0())}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [8]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [0]
proper^#(x1) = [1] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [1] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [1] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ proper(0()) -> ok(0())
, proper^#(p(X)) -> c_15(p^#(proper(X)))
, p^#(mark(X)) -> c_10(p^#(X))
, p^#(ok(X)) -> c_19(p^#(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ proper(0()) -> ok(0())
, proper^#(p(X)) -> c_15(p^#(proper(X)))
, p^#(mark(X)) -> c_10(p^#(X))
, p^#(ok(X)) -> c_19(p^#(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ 0_0() -> 3
, mark_0(3) -> 4
, mark_0(4) -> 4
, mark_0(9) -> 4
, ok_0(3) -> 9
, ok_0(4) -> 9
, ok_0(9) -> 9
, p^#_0(3) -> 22
, p^#_0(4) -> 22
, p^#_0(9) -> 22
, c_10_0(22) -> 22
, proper^#_0(3) -> 27
, proper^#_0(4) -> 27
, proper^#_0(9) -> 27
, c_19_0(22) -> 22}
9) { proper^#(cons(X1, X2)) ->
c_13(cons^#(proper(X1), proper(X2)))
, cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))
, cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))}
The usable rules for this path are the following:
{ proper(f(X)) -> f(proper(X))
, proper(0()) -> ok(0())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(f(X)) -> f(proper(X))
, proper(0()) -> ok(0())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2)))
, cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))
, cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [1] x1 + [1]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [1]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [1] x1 + [1]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [1] x1 + [1]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2)))}
and weakly orienting the rules
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [2]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [1] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [8]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [1] x1 + [3]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [1] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper(0()) -> ok(0())}
and weakly orienting the rules
{ proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper(0()) -> ok(0())}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [1] x1 + [9]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [4]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [1] x1 + [2]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [1] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))}
and weakly orienting the rules
{ proper(0()) -> ok(0())
, proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
0() = [4]
mark(x1) = [1] x1 + [8]
cons(x1, x2) = [1] x1 + [1] x2 + [8]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [4]
proper(x1) = [1] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [1] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [8]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [1] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [1] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))
, proper(0()) -> ok(0())
, proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ cons^#(mark(X1), X2) -> c_8(cons^#(X1, X2))
, proper(0()) -> ok(0())
, proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_17(cons^#(X1, X2))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ 0_0() -> 3
, mark_0(3) -> 4
, mark_0(4) -> 4
, mark_0(9) -> 4
, ok_0(3) -> 9
, ok_0(4) -> 9
, ok_0(9) -> 9
, cons^#_0(3, 3) -> 13
, cons^#_0(3, 4) -> 13
, cons^#_0(3, 9) -> 13
, cons^#_0(4, 3) -> 13
, cons^#_0(4, 4) -> 13
, cons^#_0(4, 9) -> 13
, cons^#_0(9, 3) -> 13
, cons^#_0(9, 4) -> 13
, cons^#_0(9, 9) -> 13
, c_8_0(13) -> 13
, proper^#_0(3) -> 27
, proper^#_0(4) -> 27
, proper^#_0(9) -> 27
, c_17_0(13) -> 13}
10)
{ proper^#(f(X)) -> c_11(f^#(proper(X)))
, f^#(ok(X)) -> c_16(f^#(X))
, f^#(mark(X)) -> c_7(f^#(X))}
The usable rules for this path are the following:
{ proper(f(X)) -> f(proper(X))
, proper(0()) -> ok(0())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(f(X)) -> f(proper(X))
, proper(0()) -> ok(0())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, proper^#(f(X)) -> c_11(f^#(proper(X)))
, f^#(ok(X)) -> c_16(f^#(X))
, f^#(mark(X)) -> c_7(f^#(X))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, f^#(ok(X)) -> c_16(f^#(X))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, f^#(ok(X)) -> c_16(f^#(X))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [4]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [3]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [1]
c_11(x1) = [1] x1 + [1]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [1] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{f^#(mark(X)) -> c_7(f^#(X))}
and weakly orienting the rules
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, f^#(ok(X)) -> c_16(f^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f^#(mark(X)) -> c_7(f^#(X))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [2]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [1]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [1]
c_11(x1) = [1] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [1] x1 + [1]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper^#(f(X)) -> c_11(f^#(proper(X)))}
and weakly orienting the rules
{ f^#(mark(X)) -> c_7(f^#(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, f^#(ok(X)) -> c_16(f^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(f(X)) -> c_11(f^#(proper(X)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [1]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_11(x1) = [1] x1 + [1]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [1] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper(0()) -> ok(0())}
and weakly orienting the rules
{ proper^#(f(X)) -> c_11(f^#(proper(X)))
, f^#(mark(X)) -> c_7(f^#(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, f^#(ok(X)) -> c_16(f^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper(0()) -> ok(0())}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [4]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [1]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [5]
c_11(x1) = [1] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [1] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ proper(0()) -> ok(0())
, proper^#(f(X)) -> c_11(f^#(proper(X)))
, f^#(mark(X)) -> c_7(f^#(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, f^#(ok(X)) -> c_16(f^#(X))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ proper(0()) -> ok(0())
, proper^#(f(X)) -> c_11(f^#(proper(X)))
, f^#(mark(X)) -> c_7(f^#(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, f^#(ok(X)) -> c_16(f^#(X))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ 0_0() -> 3
, mark_0(3) -> 4
, mark_0(4) -> 4
, mark_0(9) -> 4
, ok_0(3) -> 9
, ok_0(4) -> 9
, ok_0(9) -> 9
, f^#_0(3) -> 15
, f^#_0(4) -> 15
, f^#_0(9) -> 15
, c_7_0(15) -> 15
, proper^#_0(3) -> 27
, proper^#_0(4) -> 27
, proper^#_0(9) -> 27
, c_16_0(15) -> 15}
11)
{active^#(s(X)) -> c_5(s^#(active(X)))}
The usable rules for this path are the following:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, active^#(s(X)) -> c_5(s^#(active(X)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [4]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [9]
s^#(x1) = [1] x1 + [11]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active^#(s(X)) -> c_5(s^#(active(X)))}
and weakly orienting the rules
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(s(X)) -> c_5(s^#(active(X)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [5]
s^#(x1) = [1] x1 + [1]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)}
and weakly orienting the rules
{ active^#(s(X)) -> c_5(s^#(active(X)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [8]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
s^#(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, active^#(s(X)) -> c_5(s^#(active(X)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, active^#(s(X)) -> c_5(s^#(active(X)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ 0_0() -> 3
, mark_0(3) -> 4
, mark_0(4) -> 4
, mark_0(9) -> 4
, ok_0(3) -> 9
, ok_0(4) -> 9
, ok_0(9) -> 9
, active^#_0(3) -> 11
, active^#_0(4) -> 11
, active^#_0(9) -> 11
, s^#_0(3) -> 20
, s^#_0(4) -> 20
, s^#_0(9) -> 20}
12)
{active^#(p(X)) -> c_6(p^#(active(X)))}
The usable rules for this path are the following:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, active^#(p(X)) -> c_6(p^#(active(X)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{active^#(p(X)) -> c_6(p^#(active(X)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(p(X)) -> c_6(p^#(active(X)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
and weakly orienting the rules
{active^#(p(X)) -> c_6(p^#(active(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [4]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [3]
p^#(x1) = [1] x1 + [1]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)}
and weakly orienting the rules
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, active^#(p(X)) -> c_6(p^#(active(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, active^#(p(X)) -> c_6(p^#(active(X)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, active^#(p(X)) -> c_6(p^#(active(X)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ 0_0() -> 3
, mark_0(3) -> 4
, mark_0(4) -> 4
, mark_0(9) -> 4
, ok_0(3) -> 9
, ok_0(4) -> 9
, ok_0(9) -> 9
, active^#_0(3) -> 11
, active^#_0(4) -> 11
, active^#_0(9) -> 11
, p^#_0(3) -> 22
, p^#_0(4) -> 22
, p^#_0(9) -> 22}
13)
{active^#(f(X)) -> c_3(f^#(active(X)))}
The usable rules for this path are the following:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, active^#(f(X)) -> c_3(f^#(active(X)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{active^#(f(X)) -> c_3(f^#(active(X)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(f(X)) -> c_3(f^#(active(X)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_2() = [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
and weakly orienting the rules
{active^#(f(X)) -> c_3(f^#(active(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [3]
c_2() = [0]
c_3(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)}
and weakly orienting the rules
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, active^#(f(X)) -> c_3(f^#(active(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [8]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_2() = [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, active^#(f(X)) -> c_3(f^#(active(X)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(f(X)) -> f(active(X))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(s(X)) -> s(active(X))
, active(p(X)) -> p(active(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ active(f(0())) -> mark(cons(0(), f(s(0()))))
, active(f(s(0()))) -> mark(f(p(s(0()))))
, active(p(s(X))) -> mark(X)
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, active^#(f(X)) -> c_3(f^#(active(X)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ 0_0() -> 3
, mark_0(3) -> 4
, mark_0(4) -> 4
, mark_0(9) -> 4
, ok_0(3) -> 9
, ok_0(4) -> 9
, ok_0(9) -> 9
, active^#_0(3) -> 11
, active^#_0(4) -> 11
, active^#_0(9) -> 11
, f^#_0(3) -> 15
, f^#_0(4) -> 15
, f^#_0(9) -> 15}
14)
{proper^#(f(X)) -> c_11(f^#(proper(X)))}
The usable rules for this path are the following:
{ proper(f(X)) -> f(proper(X))
, proper(0()) -> ok(0())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(f(X)) -> f(proper(X))
, proper(0()) -> ok(0())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, proper^#(f(X)) -> c_11(f^#(proper(X)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [8]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [1]
c_11(x1) = [1] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper^#(f(X)) -> c_11(f^#(proper(X)))}
and weakly orienting the rules
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(f(X)) -> c_11(f^#(proper(X)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [4]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [3]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_11(x1) = [1] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper(0()) -> ok(0())}
and weakly orienting the rules
{ proper^#(f(X)) -> c_11(f^#(proper(X)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper(0()) -> ok(0())}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [4]
0() = [3]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [4]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [8]
c_11(x1) = [1] x1 + [1]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ proper(0()) -> ok(0())
, proper^#(f(X)) -> c_11(f^#(proper(X)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ proper(0()) -> ok(0())
, proper^#(f(X)) -> c_11(f^#(proper(X)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ 0_0() -> 3
, mark_0(3) -> 4
, mark_0(4) -> 4
, mark_0(9) -> 4
, ok_0(3) -> 9
, ok_0(4) -> 9
, ok_0(9) -> 9
, f^#_0(3) -> 15
, f^#_0(4) -> 15
, f^#_0(9) -> 15
, proper^#_0(3) -> 27
, proper^#_0(4) -> 27
, proper^#_0(9) -> 27}
15)
{proper^#(p(X)) -> c_15(p^#(proper(X)))}
The usable rules for this path are the following:
{ proper(f(X)) -> f(proper(X))
, proper(0()) -> ok(0())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(f(X)) -> f(proper(X))
, proper(0()) -> ok(0())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, proper^#(p(X)) -> c_15(p^#(proper(X)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [8]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [1]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [1]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [1] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper^#(p(X)) -> c_15(p^#(proper(X)))}
and weakly orienting the rules
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(p(X)) -> c_15(p^#(proper(X)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [4]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [1] x1 + [2]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper(0()) -> ok(0())}
and weakly orienting the rules
{ proper^#(p(X)) -> c_15(p^#(proper(X)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper(0()) -> ok(0())}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
0() = [15]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [8]
s(x1) = [1] x1 + [4]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [8]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [1] x1 + [1]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ proper(0()) -> ok(0())
, proper^#(p(X)) -> c_15(p^#(proper(X)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ proper(0()) -> ok(0())
, proper^#(p(X)) -> c_15(p^#(proper(X)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ 0_0() -> 3
, mark_0(3) -> 4
, mark_0(4) -> 4
, mark_0(9) -> 4
, ok_0(3) -> 9
, ok_0(4) -> 9
, ok_0(9) -> 9
, p^#_0(3) -> 22
, p^#_0(4) -> 22
, p^#_0(9) -> 22
, proper^#_0(3) -> 27
, proper^#_0(4) -> 27
, proper^#_0(9) -> 27}
16)
{proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2)))}
The usable rules for this path are the following:
{ proper(f(X)) -> f(proper(X))
, proper(0()) -> ok(0())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(f(X)) -> f(proper(X))
, proper(0()) -> ok(0())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [1] x1 + [1]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper(0()) -> ok(0())}
and weakly orienting the rules
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper(0()) -> ok(0())}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [5]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [3]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [13]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [1] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ proper(0()) -> ok(0())
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ proper(0()) -> ok(0())
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, proper^#(cons(X1, X2)) -> c_13(cons^#(proper(X1), proper(X2)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ 0_0() -> 3
, mark_0(3) -> 4
, mark_0(4) -> 4
, mark_0(9) -> 4
, ok_0(3) -> 9
, ok_0(4) -> 9
, ok_0(9) -> 9
, cons^#_0(3, 3) -> 13
, cons^#_0(3, 4) -> 13
, cons^#_0(3, 9) -> 13
, cons^#_0(4, 3) -> 13
, cons^#_0(4, 4) -> 13
, cons^#_0(4, 9) -> 13
, cons^#_0(9, 3) -> 13
, cons^#_0(9, 4) -> 13
, cons^#_0(9, 9) -> 13
, proper^#_0(3) -> 27
, proper^#_0(4) -> 27
, proper^#_0(9) -> 27}
17)
{proper^#(s(X)) -> c_14(s^#(proper(X)))}
The usable rules for this path are the following:
{ proper(f(X)) -> f(proper(X))
, proper(0()) -> ok(0())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(f(X)) -> f(proper(X))
, proper(0()) -> ok(0())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, proper^#(s(X)) -> c_14(s^#(proper(X)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, proper^#(s(X)) -> c_14(s^#(proper(X)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, proper^#(s(X)) -> c_14(s^#(proper(X)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [8]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
s(x1) = [1] x1 + [1]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [4]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper(0()) -> ok(0())}
and weakly orienting the rules
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, proper^#(s(X)) -> c_14(s^#(proper(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper(0()) -> ok(0())}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [4]
s(x1) = [1] x1 + [8]
p(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ proper(0()) -> ok(0())
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, proper^#(s(X)) -> c_14(s^#(proper(X)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(f(X)) -> f(proper(X))
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(p(X)) -> p(proper(X))
, f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))}
Weak Rules:
{ proper(0()) -> ok(0())
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, proper^#(s(X)) -> c_14(s^#(proper(X)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ 0_0() -> 3
, mark_0(3) -> 4
, mark_0(4) -> 4
, mark_0(9) -> 4
, ok_0(3) -> 9
, ok_0(4) -> 9
, ok_0(9) -> 9
, s^#_0(3) -> 20
, s^#_0(4) -> 20
, s^#_0(9) -> 20
, proper^#_0(3) -> 27
, proper^#_0(4) -> 27
, proper^#_0(9) -> 27}
18)
{active^#(f(0())) -> c_0(cons^#(0(), f(s(0()))))}
The usable rules for this path are the following:
{ f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))
, active^#(f(0())) -> c_0(cons^#(0(), f(s(0()))))}
Details:
We apply the weight gap principle, strictly orienting the rules
{active^#(f(0())) -> c_0(cons^#(0(), f(s(0()))))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(f(0())) -> c_0(cons^#(0(), f(s(0()))))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [1]
0() = [2]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [0] x1 + [0] x2 + [0]
s(x1) = [1] x1 + [1]
p(x1) = [0] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [4]
c_0(x1) = [1] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))}
Weak Rules: {active^#(f(0())) -> c_0(cons^#(0(), f(s(0()))))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ f(mark(X)) -> mark(f(X))
, s(mark(X)) -> mark(s(X))
, f(ok(X)) -> ok(f(X))
, s(ok(X)) -> ok(s(X))}
Weak Rules: {active^#(f(0())) -> c_0(cons^#(0(), f(s(0()))))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ 0_0() -> 3
, mark_0(3) -> 4
, mark_0(4) -> 4
, mark_0(9) -> 4
, ok_0(3) -> 9
, ok_0(4) -> 9
, ok_0(9) -> 9
, active^#_0(3) -> 11
, active^#_0(4) -> 11
, active^#_0(9) -> 11
, cons^#_0(3, 3) -> 13
, cons^#_0(3, 4) -> 13
, cons^#_0(3, 9) -> 13
, cons^#_0(4, 3) -> 13
, cons^#_0(4, 4) -> 13
, cons^#_0(4, 9) -> 13
, cons^#_0(9, 3) -> 13
, cons^#_0(9, 4) -> 13
, cons^#_0(9, 9) -> 13}
19)
{active^#(f(s(0()))) -> c_1(f^#(p(s(0()))))}
The usable rules for this path are the following:
{ s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))
, active^#(f(s(0()))) -> c_1(f^#(p(s(0()))))}
Details:
We apply the weight gap principle, strictly orienting the rules
{active^#(f(s(0()))) -> c_1(f^#(p(s(0()))))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(f(s(0()))) -> c_1(f^#(p(s(0()))))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
0() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [0] x1 + [0] x2 + [0]
s(x1) = [1] x1 + [1]
p(x1) = [1] x1 + [1]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [8]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))}
Weak Rules: {active^#(f(s(0()))) -> c_1(f^#(p(s(0()))))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ s(mark(X)) -> mark(s(X))
, p(mark(X)) -> mark(p(X))
, s(ok(X)) -> ok(s(X))
, p(ok(X)) -> ok(p(X))}
Weak Rules: {active^#(f(s(0()))) -> c_1(f^#(p(s(0()))))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ 0_0() -> 3
, mark_0(3) -> 4
, mark_0(4) -> 4
, mark_0(9) -> 4
, ok_0(3) -> 9
, ok_0(4) -> 9
, ok_0(9) -> 9
, active^#_0(3) -> 11
, active^#_0(4) -> 11
, active^#_0(9) -> 11
, f^#_0(3) -> 15
, f^#_0(4) -> 15
, f^#_0(9) -> 15}
20)
{active^#(p(s(X))) -> c_2()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
0() = [0]
mark(x1) = [0] x1 + [0]
cons(x1, x2) = [0] x1 + [0] x2 + [0]
s(x1) = [0] x1 + [0]
p(x1) = [0] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {active^#(p(s(X))) -> c_2()}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{active^#(p(s(X))) -> c_2()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(p(s(X))) -> c_2()}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
0() = [0]
mark(x1) = [0] x1 + [0]
cons(x1, x2) = [0] x1 + [0] x2 + [0]
s(x1) = [1] x1 + [0]
p(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {active^#(p(s(X))) -> c_2()}
Details:
The given problem does not contain any strict rules
21)
{proper^#(0()) -> c_12()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
0() = [0]
mark(x1) = [0] x1 + [0]
cons(x1, x2) = [0] x1 + [0] x2 + [0]
s(x1) = [0] x1 + [0]
p(x1) = [0] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {proper^#(0()) -> c_12()}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{proper^#(0()) -> c_12()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(0()) -> c_12()}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
0() = [0]
mark(x1) = [0] x1 + [0]
cons(x1, x2) = [0] x1 + [0] x2 + [0]
s(x1) = [0] x1 + [0]
p(x1) = [0] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_2() = [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [1]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
c_15(x1) = [0] x1 + [0]
c_16(x1) = [0] x1 + [0]
c_17(x1) = [0] x1 + [0]
c_18(x1) = [0] x1 + [0]
c_19(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_20(x1) = [0] x1 + [0]
c_21(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {proper^#(0()) -> c_12()}
Details:
The given problem does not contain any strict rules